Nuprl Lemma : hd_l_interval 11,40

T:Type, l:(T List), i:{0..||l||}, j:{0..i}. hd(l_interval(l;j;i)) = l[j T 
latex


Definitionsx:AB(x), t  T, l[i], nth_tl(n;as), Y, if b then t else f fi , i j, b, i <z j, tt, ff, {i..j}, P  Q, P  Q, i  j < k, P & Q, P  Q, , T, True, A  B, A, False
Lemmasint seg wf, length wf1, select l interval, le wf, select wf, squash wf

origin